Inference at * 
Iof proof for Lemma adjacent wf:


  T:Type, L:(T List), x, y:T. adjacent(T;L;x;y)   

latex

 by ((Unfold `adjacent` 0) 
CollapseTHEN (MaAuto)) 

latex

C.

Definitions	adjacent(T;L;x;y), x:A. B(x), #$n, , l[i], x:A. B(x), x:AB(x), Void, x:A  B(x), {i..j}, {x:A| B(x)} , , i  j < k, A  B, P & Q, A, False, P  Q, a < b, n - m, -n, n+m, ||as||, type List, s = t, t  T, Type
Lemmas	member wf, int seg wf, length wf1, select wf